In the field of computer software testing, different approaches have been developed to more accurately and completely test program function. For example, program modeling and model checking allow certain kinds of debugging analysis that may not otherwise be possible or practical in direct analysis of a program. Program models simplify certain aspects of programs to facilitate more complete testing of their overall behavior. Program models can be used to analyze programs as a whole, or, for larger programs, to analyze them one part at a time. When errors are found, changes can then be made to the program source code to correct the errors.
One kind of program modeling is predicate abstraction. Predicate abstraction models the behavior of a program using Boolean predicates, which represent conditions in the program being modeled (the “source program”) that can be evaluated as “true” or “false.” For example, the Boolean predicate (x>0) evaluates to “true” if the variable x has a positive value in a given program state, and evaluates to “false” otherwise. Predicates can be drawn from conditional statements and assertions in a source program, or from other sources. Predicate abstraction can be done automatically using an automatic predicate abstraction tool, with programmer analysis, or with some combination of tools and programmer analysis.
The product of predicate abstraction is typically a finite-state program (also referred to as a Boolean program) that models behavior of the source program. The finite-state program is an abstraction of the source program to the extent that properties satisfied in the finite-state program are satisfied in the source program.
The predicate abstraction process is complex. Typically, tools called theorem provers are used to determine whether a particular formula (derived from a source program) is implied by some Boolean combination over a set of predicates P. However, in prior predicate abstraction methods, the number of calls to a theorem prover needed to make a determination for a particular formula would increase exponentially as the number of predicates in P increased, making such methods inefficient and expensive in terms of computing resources. Other methods have used heuristics to reduce the number of calls to theorem provers in an attempt to gain efficiency by sacrificing precision.